Schreiber Topological Quantum Gates in Homotopy Type Theory

An article that we have written:

---

• David Jaz Myers, $\;$ Hisham Sati $\,$ and $\,$ Urs Schreiber:

  
  

  Topological Quantum Gates in Homotopy Type Theory

  
  

  Comm. Math. Phys. 405 172 (2024)

  doi:10.1007/s00220-024-05020-8

  
  

  download:

  • pdf

  • arXiv:2303.02382

  
  

  Abstract. Despite the plausible necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky, both regarding their (elusive) physical realization as well as their quantum information-theoretic nature. Building on recent results on defect branes in string/M-theory [SS23a] and on their holographically dual anyonic defects in condensed matter theory [SS23b], here we explain (as announced in [SS22]) how the specification of realistic topological quantum gates, operating by anyon defect braiding in topologically ordered quantum materials, has a surprisingly slick formulation in parameterized point-set topology, which is so fundamental that it lends itself to certification in modern homotopically typed programming languages, such as cubical Agda.

  We propose that this remarkable confluence of concepts may jointly kickstart the development of topological quantum programming proper as well as the real-world application of homotopy type theory, both of which have arguably been falling behind their high expectations; in any case it provides a powerful paradigm for simulating and verifying topological quantum computing architectures with high-level certification languages aware of the actual physical principles of realistic topological quantum hardware.

  In a companion article (announced earlier) we explain how further passage to "dependent linear" homotopy types naturally extends this scheme to a full-blown quantum programming/certification language in which our topological quantum gates may be compiled into verified quantum circuits with quantum measurement gates and classical control.

---

Companion articles:

• Entanglement of Sections

• The Quantum Monadology

• Quantum and Reality

Expository talks:

• Topological Quantum Programming via Linear Homotopy Types

  presentation at Quantum Physics and Logic (QPL 2024), Buenes Aires, 15 July 2024

• Topological Quantum Programming in TED-K

  talk at: PlanQC 2022

  talk slides: pdf, video: YT

• Topological Quantum Gates in HoTT

  talk at QFT and Cobordism 2023,

  NYU Abu Dhabi, March 2023

  video: YT

• Topological Quantum Programming via Linear Homotopy Types

  talk at: Homotopy Type Theory Electronic Seminar,

  01 Feb 2024

  video: YT

  Abstract. It is interesting to observe that a use-case of what deserves to be called genuine “homotopical computation” is secretly known: We showed in arXiv:2303.02382 (in print at Comm. Math. Phys) that the specification of the logic gates envisioned in “topological quantum computation on anyons”, while intricate in traditional language, have a slick expression in HoTT, simply as transport of certain truncated dependent function types into Eilenberg-MacLane types. The mathematical theorems behind this are a remarkable result on conformal quantum field theory by Feigin, Schechtmann & Varchenko (1994) combined with our novel algebro-topological construction, lending itself to formalization in HoTT, of Gauss-Manin connections on fibrations of twisted cohomology groups.

  Generally, the relation between HoTT and quantum computation is closer than might be suspected: Adding rules meant to enforce interpretation of HoTT into infinity-topoi of parameterized module spectra (such as in Riley‘s Linear HoTT) naturally provides for an expressive certification-language for quantum programming with “dynamic lifting” of quantum measurement results (arXiv:2310.15735), previously elusive but arguably necessary for any serious quantum computation.

  This is joint work with David J. Myers and Hisham Sati.

Script:

Gauss-Manin connections on twisted cohomology in traditional literature.	pdf	p. 231 in Voisin
Gauss-Manin connection on twisted cohomology as dependent function type transport.	pdf	p. 69 in TQG
Configuration spaces, braid groups and their finite presentations.	pdf	pp. 13 in TQG
KZ-connection on $\mathfrak{su}(2)$-anyonic conformal blocks as dependent function type transport.	pdf	p. 76 in TQG
Identified via FSV94‘s hypergeometric integral-construction of Laughlin wavefunctions.	pdf	p. 32 in Ord
The quantum adiabatic theorem and topological quantum gates.	pdf	p. 21 in TQG
Need for certified topological quantum language.	pdf	pp. 3 in Tow
A case for linear homotopy type theory.	pdf	pp. 3 in QM
Quantum modalities from dependent linear types.	pdf	pp. 69 in QM
(Deferred) Quantum measurement from Quantum modalities.	pdf	pp. 78 in QM
Doubly monoidal model category for dependent linearly-typed topological quantum gates.	pdf	pp. 1 in EoS

Related articles:

• Topological Quantum Programming in TED-K

  PlanQC 2022 33 (2022)

  [arXiv:2209.08331, video presentation: YT]

• Anyonic defect branes in TED-K-theory

  Rev. Math. Phys. (2023)

  [arXiv:2203.11838]

• Anyonic topological order in TED K-theory

  Rev. Math. Phys. (2023)

  [arXiv:2206.13563]

• pdf

Related talks:

• Towards Certified Topological Quantum Programming via Linear Homotopy Types,

  talk at Quantum Information and Quantum Matter 2024,

  NYU Abu Dhabi, 27-31 May 2024

• Towards Quantum Programming via Linear Homotopy Types,

  talk at Homotopy Type Theory and Computing – Classical and Quantum,

  CQTS @ New York University Abu Dhabi, 19-21 April 2024

• Topological Quantum Programming via Linear Homotopy Types

  talk at: Homotopy Type Theory Electronic Seminar (01 Feb 2024)

  [video:YT, script:web]

• Towards verified topological hardware-aware quantum programming

  slides: pdf (view on full screen)

  talk at CQTS & TII Workshop 2023

  NYU Abu Dhabi, 24 Feb 2023

• TED K-theory of Cohomotopy moduli spaces and Anyonic Topological Order

  talk at Higher Structures and Field Theory,

  ESI Vienna, 25 Aug 2022

• Quantum Data Types via Linear Homotopy Type Theory

  talk at Workshop on Quantum Software @ QTML 2022

  Naples, 12 Nov 2022

  slides: pdf (view on full screen)

• Topological Quantum Gates from M-Theory

  talk at M-Theory and Mathematics 2023

  NYU Abu Dhabi, Jan 2023

• Effective Quantum Certification via Linear Homotopy Types,

  talk at Colloquium of the Topos Institute,

  Part I: 13 April 2023, Part II: 24 Aug 2023

  slides: pdf (view full screen) video1: YT, video2: YT